$\forall$${\it es}$:ES, ${\it ff}$:FIFO, ${\it f2f+}$:F2F+{-}decls, ${\it sndr}$, ${\it rcvr}$:${\it ff}$.C. f2f+{-}p+ $\in$ E$\rightarrow$E$\rightarrow\mathbb{P}$